A:Type, eq:EqDecider(A), P:(AType), x:A, v:Type.
ydom(x : v). w=x : v(y)   P(y,w)  P(x,v) 

latex

Definitions	x. t(x), P  Q, False, True, P & Q, P  Q, P  Q, p q, eqof(d), ff, t  T, x  dom(f), f(x), b, EqDecider(T), , x:A. B(x), x(s), P  Q, xdom(f). v=f(x)   P(x;v), x : v, x(s1,s2)
Lemmas	deq wf, bfalse wf, eqof wf, bor wf, assert wf, eqof eq btrue, deq property, assert of bor, subtype rel self